The present invention relates to methods and apparatuses for improving the efficiency of a computer-implemented Boolean satisfiability solver that could be used in a model checking process. In the process of model checking, the technical design of a system, for example a circuit design written in Verilog, is translated into a Boolean formula and given to a Boolean satisfiability solver as input.